package systemfnomabss.syntax
/*
trait SystemFNomAbsSyntax { self: Binding with Substitution with BindingSyntax with AbstractSyntax with SystemFNomAbsSyntax =>
  //sealed abstract class LTerm extends Substable[LTerm, LTerm] with Substable[LType, LTerm] with Nominal[LTerm]
 
  type Term = LTerm
  type Type = LType
  sealed abstract class LTerm extends Nominal[LTerm]
  sealed trait BaseValue extends LTerm {
    def baseType: LType
    //val name: String
    //def swap(a: Name, b: Name): Self
    def fresh(a: Name)=true
    def supp: List[Name]=Nil
    def swap(a: Name, b: Name) = this
    //def subst(sub: Name => Option[LTerm]): AM[LTerm] = AM.result(this)
  }


  
  
        case class Tru extends LTerm with BaseValue{
          override def toString = "true"
          override def baseType = TyBool
        }
        case class Fls extends LTerm with BaseValue{
          override def toString= "false"
          override def baseType = TyBool
        }
        case class Unit extends LTerm with BaseValue{
          override def toString = "unit"
          override def baseType = TyUnit
        }
        case class Lit(n: int) extends LTerm with BaseValue{
          override def toString = n.toString
          override def baseType = TyInt
        }
        
  case class If(cond: LTerm, pos: LTerm, neg: LTerm) extends LTerm {
    def swap(a: Name, b: Name) = If(cond swap(a, b), pos swap(a, b), neg swap(a, b))
    def fresh(a: Name) = (cond fresh a) && (pos fresh a) && (neg fresh a)
    def supp = (cond supp) ::: (pos supp) ::: (neg supp)
  }
  
  case class Var(n: Name) extends LTerm {
    def swap(a: Name, b: Name) = Var(n swap(a, b))    
    def fresh(a: Name) = n fresh(a)
    def supp = n supp

  }
  
  case class App(fun: LTerm, arg: LTerm) extends LTerm {
    def swap(a: Name, b: Name) = App(fun swap(a, b), arg swap(a, b))
    def fresh(a: Name) = fun.fresh(a) && arg.fresh(a)
    def supp = fun.supp ::: arg.supp

  }
  
  case class Lam(ty:LType, abs: \\[LTerm]) extends LTerm {
    def swap(a: Name, b: Name) = Lam(ty swap(a,b),abs swap(a, b))
    def fresh(a: Name) = (ty fresh(a)) && (abs fresh(a))
    def supp = ty.supp  ::: abs.supp

  }
  
  case class TLam(abs: \\[LTerm]) extends LTerm {
    def swap(a: Name, b: Name) = TLam(abs swap(a, b))
    def fresh(a: Name) = abs fresh(a)
    def supp = abs supp
  }
    

  case class TApp(t:LTerm, ty: LType) extends LTerm {
    def swap(a: Name, b: Name) = TApp(t swap(a, b), ty swap(a, b))
    def fresh(a: Name) = t.fresh(a) && ty.fresh(a)
    def supp = t.supp ::: ty.supp
  }
  
  
  
  
  sealed abstract class LType extends Nominal[LType]


  sealed trait BaseType extends LType {
    val name: String
    //def swap(a: Name, b: Name): Self
    def fresh(a: Name)=true
    def supp: List[Name]=Nil
    def swap(a: Name, b: Name) = this
    def subst(sub: Name => Option[LType]): LType = this
  }
  case class TyBool() extends LType with BaseType
  { val name="Bool" }
  case class TyInt()  extends LType with BaseType
  { val name="Int"  }
  case class TyUnit() extends LType with BaseType
  { val name="Unit" }
  
  case class TyVar(n: Name) extends LType 
  { 
    def swap(a: Name, b: Name)= TyVar(n swap(a,b))
    def fresh(a: Name)= n fresh a
    def supp: List[Name]= n supp
    
    def subst(sub: Name => Option[LType]) : LType = sub(n).getOrElse[LType](this)
  }
  case class TyArr(t1: LType, t2: LType) extends LType {
    def swap(a: Name, b: Name)= TyArr(t1 swap(a,b), t2 swap(a,b))
    def fresh(a: Name)= (t1 fresh a) && (t2 fresh a)
    def supp: List[Name]= (t1 supp) ::: (t2 supp) 
    
    /*
    def subst(sub: Name => Option[LType]) : LType = 
    { val t1b = t1 subst sub;
      val t2b = t2 subst sub;
      TyArr(t1b,t2b) }
      */

  }
  case class TyUniv(abs: \\[LType]) extends LType  {
    def swap(a: Name, b: Name) = TyUniv(abs swap(a,b))
    def fresh(a: Name) = abs fresh(a)
    def supp = abs supp
    /*
    def subst(sub: Name => Option[LType]): LType = {
        val abs2 = (new AbsSubstTo[LType].AbsIsSubstable(abs)) subst(sub);
        TyUniv( abs2) }
    */
  }
  case class TyExist(abs: \\[LType]) extends LType {
    def swap(a: Name, b: Name) = TyExist(abs swap(a,b))
    def fresh(a: Name) = abs fresh(a)
    def supp = abs supp
    /*
    def subst(sub: Name => Option[LType]): LType = {
        val abs2 = new AbsSubstTo[LType].AbsIsSubstable(abs) subst(sub);
        TyExist( abs2) }
    */
  }

}


*/
